『Ghosts of Departed Proofs』

2018/7

論文中に登場する「GDP」はこれのことを指す

この論文に用いられているコード

大まかな流れ

Abstract

前提条件のある関数を「Ghosts of Departed Proofs (GDP)」を用いて定義する

前提条件を満たしていることを幽霊型を用いて表す

型で表現できるので、実行時オーバーヘッドはない

特に、依存型や線形型などの強力な型システムを使わずに設計する

1 Introduction

目標は、ライブラリ作者として、人間工学的に、安全なAPIを設計すること

GDPの特徴

Properties and proofs are represented in code.

Proofs carried by phantom type parameters.

Library-controlled APIs to create proofs.

Combinators for maipulating ghost proofs.

2 Case Study 1: Sorted Lists

2つのsort済みリストをmergeする関数を、GDPで設計する

3 Case Study 2: Sharing State Threads

型安全だが、ちょっと不便

GDPを使ってSTモナドを拡張する例

4 Case Study 3: Key-value Lookups

GDPを使って、Mapをlookupする時に、keyが存在することを型で保証する

5 Case Study 4: Arbitrary Invariants

Section 2, 3, 4で示したものを統括して扱う仕組みを考える

「型に付けた型レベルの名前」と「それに付与する証明」を分離できるようにする

6 Related Work

7 Summary

Section 2までは嬉しさは理解できる

読みメモ

Abstract

前提条件のある関数をどう定義するか？

「Ghosts of Departed Proofs」という概念についての説明をする

型で済むので実行時のオーバーヘッドがない

1 Introduction

強力な型システムを使わずとも普通のHaskellの型システムで恩恵を受けられる

目標は、ライブラリ作者として、ergonimic(人間工学的)に、安全なAPIを設計すること

ここでの「安全な」とは実行時エラーを起こさないこと

ergonimicとは、利用者に過度の負担をかけないこと

GDPの利用のケーススタディ

APIの間違った使用はコンパイルエラー

いくつかのアプローチ

Ghosts of Departed Proofsの特徴

Properties and proofs are represented in code.

Proofs carried by phantom type parameters.

関数を連鎖していく時に、その証明済みの型で定義することで、安全な値が複数の関数を通っていくイメージ

幽霊型を使うことで、ランタイムのオーバーヘッドがない

Library-controlled APIs to create proofs.

ライブラリの作者は、そのAPIの動作に関する公理を導入できる唯一の存在者であるべき

型を公開せずに、関数のみを公開するみたいな話か？

Combinators for maipulating ghost proofs.

2 Case Study 1: Sorted Lists

rank2を使うことで、利用者に任意のnameを付けさせずに、nameを与えることができる

コンパイラがexistな名前をつける感じになる

nameは名前を付けた値を直接返すのではなく、「あなたがその名前のついた値で何をしたかったのか言ってください、そうすればあなたのためにそれをします」とユーザーに言う。

例

code:hs

module Sorted (Named, SortedBy, sortBy, mergeBy) where

import The

import Named

import Data.Coerce

import qualified Data.List as L

import qualified Data.List.Utils as U

newtype SortedBy comp a = SortedBy a -- compでsort済みであることを表す

instance The (SortedBy comp a) a

sortBy :: ((a -> a -> Ordering) ~~ comp) -- 名前付きcomparator. compoと名付けられたcompartorと読める

sortBy comp xs = coerce (L.sortBy (the comp) xs)

mergeBy :: ((a -> a -> Ordering) ~~ comp)

mergeBy comp xs ys =

coerce (U.mergeBy (the comp) (the xs) (the ys))

mergeBy

3つの引数からnameを取り除いて普通にmergeByしたあとに、

ランタイムから見れば、普通のmergeBy'を実行しているのと何も変わらない

sortByが一種のsmart constructorのような役割を担っている

使用する

code:Hs

gdpMain :: IO ()

gdpMain = do

name (comparing Down) $ \gt -> do -- gt::(a->a->Ordering)~name

let xs' = sortBy gt xs

ys' = sortBy gt ys

print (the (mergeBy gt xs' ys'))

比較対象として、通常のmergeBy'を使った場合

code:hs

main :: IO ()

main = do

gt = comparing Down

使用感は同じである

もちろんコンパイルエラーは出ないのでそれに気付け無い！！！

ソートの方法が間違っている例

code:hs

ng = do

name compare $ \up ->

name (comparing Down) $ \down ->

in

the (mergeBy up list1 list2) -- type error!

これどうなん？

code:hs

-- comp指定してないから、miniumの結果5になって違うじゃん

miss :: IO ()

miss = do

name (comparing Down) $ \gt -> do

let xs' = sortBy gt xs

print (minimum_O1 xs')

minimum_O1 xs = case the xs of

[] -> Nothing

(x:_) -> Just x

いや、これも仕様的には正しいと言えるのか。

Downに対するミニマムだから

3 Case Study 2: Sharing State Threads

Section 3とSection 4は、あまり望ましくない例として書かれている

GDPを使ってSTモナドを拡張する

Left側では両方のメモリ内を操作できるが、Rightでは片方しか操作できないように型で制限している

code:hs

data Region = Region

type St s a = State (Region ~~ s) a

runSt :: (forall s. St s a) -> a

runSt action = name Region (evalState action)

newRef :: a -> St s (STRef s a)

newRef = undefined

readRef :: STRef s a -> St s a

readRef = undefined

writeRef :: STRef s a -> a -> St s ()

writeRef = undefined

runSt2 :: (forall s s'. St (s, s') a) -> a

runSt2 action = undefined

liftL :: St s a -> St (s,s') a

liftL = undefined

liftR :: St s' a -> St (s,s') a

liftR = undefined

share :: STRef s a -> St s (STRef (s,s') a)

share = undefined

use :: STRef (s,s') a -> STRef s a

use = undefined

symm :: STRef (s,s') a -> STRef (s',s) a

symm = undefined

stSharing :: Bool

stSharing = runSt2 $ do

(secret, ref) <- liftL $ do

unshared <- newRef 42

shared <- share =<< newRef 17

return (unshared, shared)

liftR $ do

let mine = use (symm ref)

x <- readRef mine

writeRef mine (x + 1)

liftL $ do

check <- readRef secret

return (check == 42)

4 Case Study 3: Key-value Lookups

Section 3とSection 4は、あまり望ましくない例として書かれている

Mapをlookupする時に、keyが存在することを型で保証したい

code:hs

code:hs

newtype JMap ks k v = JMap (Map k v) deriving Functor

newtype Key ks k = Key k

instance The (JMap ks k v) (Map k v)

instance The (Key ks k) k

member :: k -> JMap ks k v -> Maybe (Key ks k)

member = undefined

lookup:: Key ks k -> JMap ks k v -> v

lookup = undefined

reinsert:: Key ks k -> v -> JMap ks k v -> JMap ks k v

reinsert = undefined

withMap:: Map k v -> (forall ks. JMap ks k v -> t) -> t

withMap _ _ = undefined

Key ks k

JMap ks k v

withMap

ksをMapにアタッチする

member

keyがksに存在するかどうか判定

lookup

安全なlookup

特定のkは、一つのMapの中にのみ属すことも保証する

5 Case Study 4: Arbitrary Invariants

これまで2種類の方法を示した

「型に付けた型レベルの名前」と「それに付与する証明」を分離できるようにする

これを使うことで、任意の条件を幽霊型として符号化できる

code:hs

gdpHead xs = head (the xs)

(上記のコードでは使いまわしてはいない)

でもこれ、結局パターンマッチ出てるし、そんなに嬉しいか？

エンドユーザーは知る必要はない

普通に使える

6 Related Work

7 Summary

headに関してGhosts of Departed Proofsを使う嬉しさは何なのか